Nuprl Lemma : can-apply-pred?
11,40
postcript
pdf
es
:event_system{i:l},
e
:es-E(
es
). sqequal(can-apply(es-pred?(
es
);
e
); (
es-first(
es
;
e
)))
latex
Definitions
event_system{i:l}
,
t
T
,
x
:
A
.
B
(
x
)
,
es-E(
es
)
,
,
Unit
,
Type
,
b
,
A
,
b
,
s
=
t
,
prop{i:l}
,
x
:
A
B
(
x
)
,
P
Q
,
x
:
A
B
(
x
)
,
P
Q
,
P
Q
,
left
+
right
,
first(
e
)
,
es-first(
es
;
e
)
,
can-apply(
f
;
x
)
,
es-pred?(
es
)
,
f
(
a
)
,
isl(
x
)
Lemmas
eqtt
to
assert
,
iff
transitivity
,
eqff
to
assert
,
assert
of
bnot
,
bnot
wf
,
not
wf
,
assert
wf
,
isl
wf
,
unit
wf
,
es-pred?
wf
,
bool
wf
,
es-E
wf
,
event
system
wf
origin
es:event_system{i:l}, e:es-E(es). sqequal(can-apply(es-pred?(es); e); (
es-first(es; e))) es:event_system{i:l}, e:es-E(es). sqequal(can-apply(es-pred?(es); e); (es-first(es; e))) 
Tx:A. B(x)
bAb
B(x)
Q
B(x)
Q
Q